es:ES, e:E. first(e)  state after pred(e) = (state when e)  state@loc(e) 

latex

Definitions

let x = a in b(x), Id, f(a), x:AB(x), pred(e), when-after(e;info;pred?;init;Trans;val), 2of(t), <a,b>, x:AB(x), 1of(t), state@i, s = t, x:A. B(x), t  T, b, A, b, , Prop, False, P  Q, first(e), P & Q, P  Q, Unit, left+right, es_val(es), es-Trans(es), es_init(es), es-pred?(es), es_info(es), (state when e), state after e, pred(e), loc(e), first(e), E, ES, {T}, SQType(T), es-T(es), vartype(i;x), x. t(x), A & B, EOrderAxioms(E; pred?; info), loc(e), s ~ t

Lemmas

when-after wf, pred wf, pi2 wf, Id sq, subtype rel self, loc wf, Id wf, event system wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, first wf, bool wf, bnot wf, not wf, assert wf